T:Type, dT:EqDecider(T), L:(T List), x:T. (x  L)  (L[index(L;x)] = x) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), (x  l), P  Q, P & Q, {i..j}, b, x:A. B(x), i  j , False, A, A  B, , {T}, index(L;x), l[i], eqof(d), f(a), x.A(x), ||as||, P  Q, P  Q, i  j < k, A c B, mu(f)
Lemmas	l index wf, mu wf, nat wf, assert wf, le wf, deq property, mu-bound-property, non neg length, length wf1, eqof wf, select wf, int seg wf, l member wf, deq wf